(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "arithmetics/nat.ma".
include "basics/lists/list.ma".


  
inductive operator : Type[0] ≝
  par : operator
| copar : operator
| seq : operator.  

inductive struct : Type[0] ≝
|  atom : nat → struct
|  lista : operator → list struct → struct.

notation "x+" with precedence 80 for @{(atom $x)}.  

inductive sub_struct : struct → struct → Prop ≝
| it : ∀S. sub_struct S S
| inner : ∀S,S1,O,l. sub_struct S S1 → mem ? S1 l → sub_struct S (lista O l).

lemma sub_atom: ∀S,n. sub_struct S (n+) → S = n+.
#S #n #Hsub inversion Hsub // #S1 #S2 #S3 #l #_ #_ #_ #_ #H destruct
qed.

lemma sub_list: ∀n,O,l.  sub_struct (n+) (lista O l) → 
  ∃S. mem ? S l ∧ sub_struct (n+) S.
#n #O #l #Hsub inversion Hsub 
  [#S #Heq <Heq #Habs destruct
  |#S #S1 #Op #l1 #Hsub #Hmem #_ #_ #Heq destruct (Heq) %{S1} % // 
  ]
qed. 

notation "x ≡ y" with precedence 45
  for @{struct_eq $x $y}.

inductive struct_eq : struct→ struct → Prop ≝ 
 | eqRif : ∀S1 .                  S1 ≡ S1
 | eqAss : ∀L1,L2,L3.∀O:operator. lista O (L1@L2@L3) ≡ lista O (L1@((lista O L2)::L3))  
 | eqComm : ∀S1,S2 .              S2 ≡ S1 → S1≡ S2
 | eqTrans : ∀S1,S2,S3.           S1 ≡ S2 → S2 ≡ S3 → S1 ≡ S3 
 | eqSingleton : ∀O.∀S.           lista O [S] ≡ S.

lemma sub1 : ∀S,S1.S≡S1 → ∀n.sub_struct (n+) S \liff  sub_struct (n+) S1.
#S #S1 #H elim H
  [/2/
  |#L1 #L2 #L3 #O #n %  
    [#e1 cases (sub_list …e1) #Sx * #Hmem #Hsub
     cases (mem_append ???? Hmem) -Hmem
      [#Hmem1 @(inner … Hsub) @mem_append_l1 //
      |#Hmem2 cases (mem_append ???? Hmem2) -Hmem2
        [#Hmem2 @(inner ? (lista O L2)) 
          [@(inner … Hsub) // | @mem_append_l2 %1 //]
        |#mem3 @(inner … Hsub) @mem_append_l2 %2 //
        ]
      ]
    |#e1 cases (sub_list …e1) #Sx * #Hmem #Hsub
     cases (mem_append ???? Hmem) -Hmem
      [#Hmem1 @(inner … Hsub) @mem_append_l1 //
      |* 
        [#HSx >HSx in Hsub; -HSx #e2 cases (sub_list …e2)
         #Sy * #HmemSy #HsubSy @(inner … HsubSy) 
         @mem_append_l2 @mem_append_l1 //
        |#mem3 @(inner … Hsub) @mem_append_l2 @mem_append_l2 //
        ]
      ]
    ]    
  |#Sx #Sy #H #Hind #n cases (Hind n) #Hind1 #Hind2 % /2/
  |#Sx #Sy #Sz #H1 #H2 #Hinda #Hindb #n 
   cases (Hinda n) #Hinda1 #Hinda2 cases (Hindb n) #Hindb1 #Hindb2 % /3/
  |#O #Sx #n % 
    [#H1 inversion H1 
      [#Sy #HSy <HSy #Habs destruct (Habs)
      |#Sy #Sz #Op #l #Hsub #Hmem #Hind #HSy #Hl destruct (Hl) 
       lapply Hmem normalize in ⊢ (%→?); * // @False_ind
      ]
    |#Hsub @(inner … Hsub) %1 //
    ]
  ]
qed.
       
lemma dd : ∀n,m. n+≡m+ → n+=m+.
#n #m #H lapply (sub1 … H n) * #H1 #_ @sub_atom @H1 // qed.

